ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). (eclbase?(x))  (eclbase-k(x)  Knd) 

latex

Definitions	x. t(x), if b then t else f fi , ff, tt, eclbase-k(x), t  T, eclbase?(x), b, P  Q, x:A. B(x), x(s), False, ecl(ds;da), eclcatch(a;l), eclthrow(a;n), a.n, [a]*, eclor(a;b), ecland(a;b), eclseq(a;b), , eclbase(k;test)
Lemmas	Id wf, Knd wf, fpf wf, ecl wf, eclbase? wf, assert wf, false wf, true wf